$\forall$$T$:Type, ${\it as}$:($T$ List), $n$:\{0$\ldots\,\parallel$${\it as}$$\parallel$\}, $i$:\{0..$n$$^{-}$\}. firstn($n$;${\it as}$)[$i$] = ${\it as}$[$i$] $\in$ $T$